AtomDeq  EqDecider(Atom) 

latex

Definitions	t  T, EqDecider(T), AtomDeq, x:A. B(x), P  Q, , P & Q, P  Q, P  Q
Lemmas	eq atom wf, iff wf, assert wf